A:Type, eq:EqDecider(A), B:(AType), L:(a:A fp B(a) List), x:A.
(x  dom((L)))
 (f,gL.  x:A. ((x  dom(f)) & (x  dom(g))))
 (f:a:A fp B(a). (f  L)  (x  dom(f))  ((L)(x) = f(x)  B(x))) 

latex

Definitions	x:A. B(x), x(s), P  Q, P & Q, t  T, , x. t(x), x,y. t(x;y), S  T, {i..j}, i  j < k, T, True, A, A  B, False, (xL.P(x)), x:A. B(x), x(s1,s2), (x  l), A c B, , Dec(P), P  Q, (x,yL.  P(x;y))
Lemmas	fpf-join-list-ap, assert wf, fpf-dom wf, fpf-trivial-subtype-top, l member wf, fpf wf, pairwise wf, not wf, fpf-join-list wf, top wf, deq wf, fpf-ap wf, decidable lt, le wf, length wf1, squash wf, select wf